『Homotopy Type Theory: Univalent Foundations of Mathematics』

https://homotopytypetheory.org/book/ (PDF)

ホモトピー型理論(Homotopy Type Theory; HoTT)の経典？のようなとてもまとまった本

『Homotopy Type Theory: Univalent Foundations of Mathematics』目次

1labというサイトがAgdaベースでHoTTを一部形式化してるので参考にしたい

The HoTT Book? - 1Lab

Introduction

P1～P14

型、論理、集合、ホモトピーの対応はHoTTの本に書いてあった。翻訳したものは下記。

$ \begin{array}{c|c|c|c} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) & 集合(\mathrm{Sets}) & ホモトピー \\ \hline A & 命題 & 集合 & 空間 \\ a: A & 証明 & 元 & 点 \\ B(x) & 述語 & 集合の族 & ファイブレーション \\ b(x) : B(x) & \mathrm{条件付き証明} & 元の族 & \mathrm{切断} \\ \bm{0, 1} & \bot , \top & \varnothing , \{ \varnothing \} & \varnothing, * \\ A + B & A \lor B & \mathrm{非交和} & 余積 \\ A \times B & A \land B & 組の集合 & 積の空間 \\ A \to B & A \implies B & 関数の集合 & 関数空間 \\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) & \mathrm{直和} & \mathrm{全空間 } \\ \prod_{(x:A)}B(x) & \forall_{x:A} B(x) & 積 & 切断の空間 \\ \mathrm{Id}_A & 等号\ = & \lbrace (x, x) | x \in A \rbrace & 道空間A^I \end{array}

ref: Table 1: Comparing points of view on type-thoretic operations (P11)

$ a :A : 項aは型Aを持つ

$ f(a) : $ a における$ f の値(value)

table:訳

英語日本語

type 型

logic 論理

homotopy ホモトピー

proposition 命題

set 集合

space 空間

proof 証明

element 元

point 点

predicate 述語

family of sets 集合の族

fibration ファイブレーション

section 断面 or 切断

conditional proof 条件付き証明

family of sets 集合の族

disjoint union 非交和

coproduct 余積

set of pairs 組の集合

product space 積の空間

set of function 関数の集合

function space 関数空間

disjoint sum 直和

total space 全空間、全体空間？

product 直積

space of section 切断の空間 or セクションの空間？

equality 等号

path space 道空間

object 対象

rule 規則

judgements 判断

deductive system 演繹系

assumption 仮定

adjoint 随伴

adjunction 随伴

pointwise 点別の

moment in time その瞬間で

analogously 類似の方法で

familiar おなじみの

homotopy colimit ホモトピー余極限

suspension 懸垂

Postnikov tower ポストニコフ塔

localization 局所化

spectrification スペクトロフィケーション？

ETCS Elementary Theory of the Category of Sets(集合の圏の初等理論)

homotopy n-types ホモトピーn型

nth Postnikov section n番目ポストニコフ断面

proof by contradiction 背理法

Propositions as Types 型としての命題？

(−1)-truncated logic

intuitionistic 直観主義

endpoint 端点

LEM Law of Excluded middle(排中律)

AC Axiom of Choice(選択公理)

cannonical mapping 自然な写像？、

Godel’s Dialectica interpretation ゲーデルのダイアレクティカ解釈

property 性質

Freudenthal suspension theorem フロイデンタールの懸垂定理

mere propositions 単命題？

universe 宇宙

identity

equivalent types

small type

contractible 可縮

transfinite 超限、有限を超える

judgmentally equal 判断として等しい

judgmental equality 判断的同値性？

definitional equality 定義的同値性？

(propositionally) equal 命題として等しい

table:訳2

英語訳

definitionally 定義上

prescribing 処方する

Unsurprisingly 当然のことながら

Constructivity 構成性

striking 顕著な

stratified 層化？

presume 〔～を〕推定する、推測する、仮定する

inchoate 不完全な、未完成の

undergraduate 学部生

Open problems 未解決の問題

宇宙(universe)$ \mathcal{U}

型$ A, B $ X \simeq Y (ホモトピー同値)

$ \mathrm{Id}_{\mathcal{U}} (A, B) = \mathrm{Equiv}(A, B)

Univalence Axiom

$ (A = B) \simeq (A \simeq B)

型宇宙

四色定理、Feit-Thompson定理

William LawvereのETCS(Elementary Theory of the Category of Sets、日: 集合の圏の初等理論)というものがある

propositional equality

AとBは同型であるというのが$ \mathrm{Iso}(A, B) ？

形式的に書くと下記になる

$ \mathrm{Iso}(A, B) :\equiv \sum_{(f:A \to B)} \sum_{(g:B \to A)}\left \lparen \lparen \prod_{(x:A)}g(f(x)) = x \rparen \times \lparen \prod_{(y:B)} f(g(y) = y)\rparen \right\rparen

型コンストラクタΣ,Π,×をそれぞれ「存在する」,「すべて存在する」,「and」と言い換えられる

Table1より

$ \begin{array}{cc} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) \\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) \\ \prod_{x:A}B(x) & \forall_{x:A} B(x) \\ A \times B & A \land B \end{array}

stratified (…に)層を形成させる、 (…を)層状にする

homotopy (−1)-typesはmere propositionss(単なる命題？)

Kol32, TvD88a, TvD88b

Kol32: Andrey Kolmogorov. Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35:58–65, 1932. (Cited on page 9.)

TvD88a: Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. Vol. I, volume 121 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. An introduction. (Cited on pages 9 and 127.)

TvD88b: Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. Vol. II, volume 123 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. An introduction. (Cited on pages 9 and 127.)

n-truncated logic

n-truncated object of an (infinity,1)-category in nLab

TV02, Rez05, Lur09

TV02: Bertrand To ̈ en and Gabriele Vezzosi. Homotopical algebraic geometry I: Topos theory, 2002. arXiv:math/0207028. (Cited on page 10.)

Rez05: Charles Rezk. Toposes and homotopy toposes. http://www.math.uiuc.edu/~rezk/homotopy-topos-sketch.pdf , 2005. (Cited on pages 10 and 146.)

https://ncatlab.org/nlab/files/Rezk_HomotopyToposes.pdf

Lur09: Jacob Lurie. Higher topos theory. Number 170 in Annals of Mathematics Studies. Princeton University Press, 2009. arXiv:math.CT/0608040. (Cited on pages 10, 146, 252, and 298.)

KLV12, LS17

KLV12: Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The simplicial model of univalent foundations, 2012. arXiv:1211.2851. (Cited on pages 11, 103, 175, and 441.)

LS17: Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. arXiv:1705.07088, 2017. (Cited on pages 11, 175, 218, and 441.)

$ \pi_1(\mathbb{S^1}) = \mathbb{Z}

Chapter 1 Type Thoery

『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 1 Type theory

Chapter 2 Homotopy type theory

『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 2 Homotopy type theory

Chapter 3 Sets and logic

『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 3 Sets and logic

Chapter 4 Equivalences

『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 4 Equivalences

Chapter 5 Induction

『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 5 Induction

Chapter 6 Higher inductive types